0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 9 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 4 ms)
↳11 QDP
↳12 MRRProof (⇔, 30 ms)
↳13 QDP
↳14 PisEmptyProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 MRRProof (⇔, 146 ms)
↳22 QDP
↳23 PisEmptyProof (⇔, 0 ms)
↳24 YES
samefringe_in_gg(nil, nil) → samefringe_out_gg(nil, nil)
samefringe_in_gg(cons(U, V), cons(X, Y)) → U2_gg(U, V, X, Y, gopher_in_ga(cons(U, V), cons(U1, V1)))
gopher_in_ga(nil, nil) → gopher_out_ga(nil, nil)
gopher_in_ga(cons(nil, Y), cons(nil, Y)) → gopher_out_ga(cons(nil, Y), cons(nil, Y))
gopher_in_ga(cons(cons(U, V), W), X) → U1_ga(U, V, W, X, gopher_in_ga(cons(U, cons(V, W)), X))
U1_ga(U, V, W, X, gopher_out_ga(cons(U, cons(V, W)), X)) → gopher_out_ga(cons(cons(U, V), W), X)
U2_gg(U, V, X, Y, gopher_out_ga(cons(U, V), cons(U1, V1))) → U3_gg(U, V, X, Y, U1, V1, gopher_in_ga(cons(X, Y), cons(X1, Y1)))
U3_gg(U, V, X, Y, U1, V1, gopher_out_ga(cons(X, Y), cons(X1, Y1))) → U4_gg(U, V, X, Y, samefringe_in_gg(V1, Y1))
U4_gg(U, V, X, Y, samefringe_out_gg(V1, Y1)) → samefringe_out_gg(cons(U, V), cons(X, Y))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
samefringe_in_gg(nil, nil) → samefringe_out_gg(nil, nil)
samefringe_in_gg(cons(U, V), cons(X, Y)) → U2_gg(U, V, X, Y, gopher_in_ga(cons(U, V), cons(U1, V1)))
gopher_in_ga(nil, nil) → gopher_out_ga(nil, nil)
gopher_in_ga(cons(nil, Y), cons(nil, Y)) → gopher_out_ga(cons(nil, Y), cons(nil, Y))
gopher_in_ga(cons(cons(U, V), W), X) → U1_ga(U, V, W, X, gopher_in_ga(cons(U, cons(V, W)), X))
U1_ga(U, V, W, X, gopher_out_ga(cons(U, cons(V, W)), X)) → gopher_out_ga(cons(cons(U, V), W), X)
U2_gg(U, V, X, Y, gopher_out_ga(cons(U, V), cons(U1, V1))) → U3_gg(U, V, X, Y, U1, V1, gopher_in_ga(cons(X, Y), cons(X1, Y1)))
U3_gg(U, V, X, Y, U1, V1, gopher_out_ga(cons(X, Y), cons(X1, Y1))) → U4_gg(U, V, X, Y, samefringe_in_gg(V1, Y1))
U4_gg(U, V, X, Y, samefringe_out_gg(V1, Y1)) → samefringe_out_gg(cons(U, V), cons(X, Y))
SAMEFRINGE_IN_GG(cons(U, V), cons(X, Y)) → U2_GG(U, V, X, Y, gopher_in_ga(cons(U, V), cons(U1, V1)))
SAMEFRINGE_IN_GG(cons(U, V), cons(X, Y)) → GOPHER_IN_GA(cons(U, V), cons(U1, V1))
GOPHER_IN_GA(cons(cons(U, V), W), X) → U1_GA(U, V, W, X, gopher_in_ga(cons(U, cons(V, W)), X))
GOPHER_IN_GA(cons(cons(U, V), W), X) → GOPHER_IN_GA(cons(U, cons(V, W)), X)
U2_GG(U, V, X, Y, gopher_out_ga(cons(U, V), cons(U1, V1))) → U3_GG(U, V, X, Y, U1, V1, gopher_in_ga(cons(X, Y), cons(X1, Y1)))
U2_GG(U, V, X, Y, gopher_out_ga(cons(U, V), cons(U1, V1))) → GOPHER_IN_GA(cons(X, Y), cons(X1, Y1))
U3_GG(U, V, X, Y, U1, V1, gopher_out_ga(cons(X, Y), cons(X1, Y1))) → U4_GG(U, V, X, Y, samefringe_in_gg(V1, Y1))
U3_GG(U, V, X, Y, U1, V1, gopher_out_ga(cons(X, Y), cons(X1, Y1))) → SAMEFRINGE_IN_GG(V1, Y1)
samefringe_in_gg(nil, nil) → samefringe_out_gg(nil, nil)
samefringe_in_gg(cons(U, V), cons(X, Y)) → U2_gg(U, V, X, Y, gopher_in_ga(cons(U, V), cons(U1, V1)))
gopher_in_ga(nil, nil) → gopher_out_ga(nil, nil)
gopher_in_ga(cons(nil, Y), cons(nil, Y)) → gopher_out_ga(cons(nil, Y), cons(nil, Y))
gopher_in_ga(cons(cons(U, V), W), X) → U1_ga(U, V, W, X, gopher_in_ga(cons(U, cons(V, W)), X))
U1_ga(U, V, W, X, gopher_out_ga(cons(U, cons(V, W)), X)) → gopher_out_ga(cons(cons(U, V), W), X)
U2_gg(U, V, X, Y, gopher_out_ga(cons(U, V), cons(U1, V1))) → U3_gg(U, V, X, Y, U1, V1, gopher_in_ga(cons(X, Y), cons(X1, Y1)))
U3_gg(U, V, X, Y, U1, V1, gopher_out_ga(cons(X, Y), cons(X1, Y1))) → U4_gg(U, V, X, Y, samefringe_in_gg(V1, Y1))
U4_gg(U, V, X, Y, samefringe_out_gg(V1, Y1)) → samefringe_out_gg(cons(U, V), cons(X, Y))
SAMEFRINGE_IN_GG(cons(U, V), cons(X, Y)) → U2_GG(U, V, X, Y, gopher_in_ga(cons(U, V), cons(U1, V1)))
SAMEFRINGE_IN_GG(cons(U, V), cons(X, Y)) → GOPHER_IN_GA(cons(U, V), cons(U1, V1))
GOPHER_IN_GA(cons(cons(U, V), W), X) → U1_GA(U, V, W, X, gopher_in_ga(cons(U, cons(V, W)), X))
GOPHER_IN_GA(cons(cons(U, V), W), X) → GOPHER_IN_GA(cons(U, cons(V, W)), X)
U2_GG(U, V, X, Y, gopher_out_ga(cons(U, V), cons(U1, V1))) → U3_GG(U, V, X, Y, U1, V1, gopher_in_ga(cons(X, Y), cons(X1, Y1)))
U2_GG(U, V, X, Y, gopher_out_ga(cons(U, V), cons(U1, V1))) → GOPHER_IN_GA(cons(X, Y), cons(X1, Y1))
U3_GG(U, V, X, Y, U1, V1, gopher_out_ga(cons(X, Y), cons(X1, Y1))) → U4_GG(U, V, X, Y, samefringe_in_gg(V1, Y1))
U3_GG(U, V, X, Y, U1, V1, gopher_out_ga(cons(X, Y), cons(X1, Y1))) → SAMEFRINGE_IN_GG(V1, Y1)
samefringe_in_gg(nil, nil) → samefringe_out_gg(nil, nil)
samefringe_in_gg(cons(U, V), cons(X, Y)) → U2_gg(U, V, X, Y, gopher_in_ga(cons(U, V), cons(U1, V1)))
gopher_in_ga(nil, nil) → gopher_out_ga(nil, nil)
gopher_in_ga(cons(nil, Y), cons(nil, Y)) → gopher_out_ga(cons(nil, Y), cons(nil, Y))
gopher_in_ga(cons(cons(U, V), W), X) → U1_ga(U, V, W, X, gopher_in_ga(cons(U, cons(V, W)), X))
U1_ga(U, V, W, X, gopher_out_ga(cons(U, cons(V, W)), X)) → gopher_out_ga(cons(cons(U, V), W), X)
U2_gg(U, V, X, Y, gopher_out_ga(cons(U, V), cons(U1, V1))) → U3_gg(U, V, X, Y, U1, V1, gopher_in_ga(cons(X, Y), cons(X1, Y1)))
U3_gg(U, V, X, Y, U1, V1, gopher_out_ga(cons(X, Y), cons(X1, Y1))) → U4_gg(U, V, X, Y, samefringe_in_gg(V1, Y1))
U4_gg(U, V, X, Y, samefringe_out_gg(V1, Y1)) → samefringe_out_gg(cons(U, V), cons(X, Y))
GOPHER_IN_GA(cons(cons(U, V), W), X) → GOPHER_IN_GA(cons(U, cons(V, W)), X)
samefringe_in_gg(nil, nil) → samefringe_out_gg(nil, nil)
samefringe_in_gg(cons(U, V), cons(X, Y)) → U2_gg(U, V, X, Y, gopher_in_ga(cons(U, V), cons(U1, V1)))
gopher_in_ga(nil, nil) → gopher_out_ga(nil, nil)
gopher_in_ga(cons(nil, Y), cons(nil, Y)) → gopher_out_ga(cons(nil, Y), cons(nil, Y))
gopher_in_ga(cons(cons(U, V), W), X) → U1_ga(U, V, W, X, gopher_in_ga(cons(U, cons(V, W)), X))
U1_ga(U, V, W, X, gopher_out_ga(cons(U, cons(V, W)), X)) → gopher_out_ga(cons(cons(U, V), W), X)
U2_gg(U, V, X, Y, gopher_out_ga(cons(U, V), cons(U1, V1))) → U3_gg(U, V, X, Y, U1, V1, gopher_in_ga(cons(X, Y), cons(X1, Y1)))
U3_gg(U, V, X, Y, U1, V1, gopher_out_ga(cons(X, Y), cons(X1, Y1))) → U4_gg(U, V, X, Y, samefringe_in_gg(V1, Y1))
U4_gg(U, V, X, Y, samefringe_out_gg(V1, Y1)) → samefringe_out_gg(cons(U, V), cons(X, Y))
GOPHER_IN_GA(cons(cons(U, V), W), X) → GOPHER_IN_GA(cons(U, cons(V, W)), X)
GOPHER_IN_GA(cons(cons(U, V), W)) → GOPHER_IN_GA(cons(U, cons(V, W)))
GOPHER_IN_GA(cons(cons(U, V), W)) → GOPHER_IN_GA(cons(U, cons(V, W)))
cons2 > GOPHERINGA1
GOPHER_IN_GA_1=1
cons_2=0
U2_GG(U, V, X, Y, gopher_out_ga(cons(U, V), cons(U1, V1))) → U3_GG(U, V, X, Y, U1, V1, gopher_in_ga(cons(X, Y), cons(X1, Y1)))
U3_GG(U, V, X, Y, U1, V1, gopher_out_ga(cons(X, Y), cons(X1, Y1))) → SAMEFRINGE_IN_GG(V1, Y1)
SAMEFRINGE_IN_GG(cons(U, V), cons(X, Y)) → U2_GG(U, V, X, Y, gopher_in_ga(cons(U, V), cons(U1, V1)))
samefringe_in_gg(nil, nil) → samefringe_out_gg(nil, nil)
samefringe_in_gg(cons(U, V), cons(X, Y)) → U2_gg(U, V, X, Y, gopher_in_ga(cons(U, V), cons(U1, V1)))
gopher_in_ga(nil, nil) → gopher_out_ga(nil, nil)
gopher_in_ga(cons(nil, Y), cons(nil, Y)) → gopher_out_ga(cons(nil, Y), cons(nil, Y))
gopher_in_ga(cons(cons(U, V), W), X) → U1_ga(U, V, W, X, gopher_in_ga(cons(U, cons(V, W)), X))
U1_ga(U, V, W, X, gopher_out_ga(cons(U, cons(V, W)), X)) → gopher_out_ga(cons(cons(U, V), W), X)
U2_gg(U, V, X, Y, gopher_out_ga(cons(U, V), cons(U1, V1))) → U3_gg(U, V, X, Y, U1, V1, gopher_in_ga(cons(X, Y), cons(X1, Y1)))
U3_gg(U, V, X, Y, U1, V1, gopher_out_ga(cons(X, Y), cons(X1, Y1))) → U4_gg(U, V, X, Y, samefringe_in_gg(V1, Y1))
U4_gg(U, V, X, Y, samefringe_out_gg(V1, Y1)) → samefringe_out_gg(cons(U, V), cons(X, Y))
U2_GG(U, V, X, Y, gopher_out_ga(cons(U, V), cons(U1, V1))) → U3_GG(U, V, X, Y, U1, V1, gopher_in_ga(cons(X, Y), cons(X1, Y1)))
U3_GG(U, V, X, Y, U1, V1, gopher_out_ga(cons(X, Y), cons(X1, Y1))) → SAMEFRINGE_IN_GG(V1, Y1)
SAMEFRINGE_IN_GG(cons(U, V), cons(X, Y)) → U2_GG(U, V, X, Y, gopher_in_ga(cons(U, V), cons(U1, V1)))
gopher_in_ga(cons(nil, Y), cons(nil, Y)) → gopher_out_ga(cons(nil, Y), cons(nil, Y))
gopher_in_ga(cons(cons(U, V), W), X) → U1_ga(U, V, W, X, gopher_in_ga(cons(U, cons(V, W)), X))
U1_ga(U, V, W, X, gopher_out_ga(cons(U, cons(V, W)), X)) → gopher_out_ga(cons(cons(U, V), W), X)
U2_GG(X, Y, gopher_out_ga(cons(U1, V1))) → U3_GG(V1, gopher_in_ga(cons(X, Y)))
U3_GG(V1, gopher_out_ga(cons(X1, Y1))) → SAMEFRINGE_IN_GG(V1, Y1)
SAMEFRINGE_IN_GG(cons(U, V), cons(X, Y)) → U2_GG(X, Y, gopher_in_ga(cons(U, V)))
gopher_in_ga(cons(nil, Y)) → gopher_out_ga(cons(nil, Y))
gopher_in_ga(cons(cons(U, V), W)) → U1_ga(gopher_in_ga(cons(U, cons(V, W))))
U1_ga(gopher_out_ga(X)) → gopher_out_ga(X)
gopher_in_ga(x0)
U1_ga(x0)
U2_GG(X, Y, gopher_out_ga(cons(U1, V1))) → U3_GG(V1, gopher_in_ga(cons(X, Y)))
U3_GG(V1, gopher_out_ga(cons(X1, Y1))) → SAMEFRINGE_IN_GG(V1, Y1)
SAMEFRINGE_IN_GG(cons(U, V), cons(X, Y)) → U2_GG(X, Y, gopher_in_ga(cons(U, V)))
POL(SAMEFRINGE_IN_GG(x1, x2)) = 2 + 2·x1 + 2·x2
POL(U1_ga(x1)) = x1
POL(U2_GG(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + 2·x3
POL(U3_GG(x1, x2)) = 1 + 2·x1 + 2·x2
POL(cons(x1, x2)) = 1 + x1 + x2
POL(gopher_in_ga(x1)) = x1
POL(gopher_out_ga(x1)) = x1
POL(nil) = 0
gopher_in_ga(cons(nil, Y)) → gopher_out_ga(cons(nil, Y))
gopher_in_ga(cons(cons(U, V), W)) → U1_ga(gopher_in_ga(cons(U, cons(V, W))))
U1_ga(gopher_out_ga(X)) → gopher_out_ga(X)
gopher_in_ga(x0)
U1_ga(x0)